perm filename IMPURE.XGP[F77,JMC] blob
sn#316829 filedate 1977-11-11 generic text, type T, neo UTF8
/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXM30/FONT#2=BAXB30/FONT#3=SUB/FONT#4=SUP/FONT#5=NGR25/FONT#6=NGR20/FONT#7=MATH30/FONT#9=GRK30/FONT#10=MS25/FONT#11=GRFX25/FONT#12=GRFX35
␈↓ ↓H␈↓␈↓ εH␈↓ 91
␈↓ ↓H␈↓α␈↓ ¬{Chapter IV
␈↓ ↓H␈↓α␈↓ βVIMPURE PROGRAMS AND UNCLEAN PROGRAMS
␈↓ ↓H␈↓ Pure␈α
clean␈α∞LISP␈α
programs␈α∞admit␈α
the␈α
elegant␈α∞mathematical␈α
characterization␈α∞described␈α
and
␈↓ ↓H␈↓applied␈α⊂in␈α⊂Chapter␈α∂3.␈α⊂ Specifically,␈α⊂each␈α∂recursively␈α⊂defined␈α⊂pure␈α∂clean␈α⊂LISP␈α⊂function␈α⊂can␈α∂be
␈↓ ↓H␈↓translated␈αinto␈αa␈αfunctional␈αequation␈αand␈αminimization␈αschema␈αin␈αa␈αfirst␈αorder␈αlanguage,␈αand␈αthe
␈↓ ↓H␈↓function and schema can be used to prove that the program meets its extensional specifications.
␈↓ ↓H␈↓ In␈α⊂this␈α∂chapter␈α⊂we␈α∂shall␈α⊂describe␈α∂some␈α⊂additional␈α∂features␈α⊂of␈α∂practical␈α⊂LISP␈α⊂systems␈α∂for
␈↓ ↓H␈↓which␈α
good␈α
simple␈α
mathematical␈α
characterizations␈α
have␈α
not␈α
yet␈α
been␈α
found.␈α
Every␈α
computation
␈↓ ↓H␈↓that␈αcan␈αbe␈αdone␈α
with␈αthese␈αfeatures␈αcan␈α
be␈αdone␈αin␈αpure␈α
clean␈αLISP,␈αbut␈αnevertheless␈α
there␈αare
␈↓ ↓H␈↓often␈α
good␈α
reasons␈α
for␈α
using␈α
these␈α
features.␈α
We␈α
shall␈α
examine␈α
the␈α
features␈α
themselves␈α∞and␈α
also
␈↓ ↓H␈↓the criteria that determine when they should be used in preference to pure clean LISP.
␈↓ ↓H␈↓ All␈α⊗these␈α⊗features␈α⊗can␈α⊗be␈α∃formalized␈α⊗in␈α⊗terms␈α⊗of␈α⊗their␈α∃effect␈α⊗on␈α⊗the␈α⊗"state␈α⊗of␈α∃the
␈↓ ↓H␈↓computation",␈αand␈αthis␈αhas␈αbeen␈αdone␈αby␈αMichael␈αGordon␈α(197x),␈αbut␈αhis␈αformalizations␈αseem␈αtoo
␈↓ ↓H␈↓complicated␈αfor␈αelementary␈αexposition.␈α The␈αgeneral␈αidea␈αis␈αto␈αintroduce␈αa␈αstate␈αvariable␈α␈↓ x␈↓␈αand␈αto
␈↓ ↓H␈↓describe the "execution" of expressions as functions on states that produce new states.
␈↓ ↓H␈↓1. ␈↓αSequential (Algol-like) programs.␈↓
␈↓ ↓H␈↓ Sequential␈α∪programs␈α∪are␈α∀impure␈α∪(by␈α∪definition),␈α∪but␈α∀can␈α∪be␈α∪clean␈α∪-␈α∀provided␈α∪certain
␈↓ ↓H␈↓restrictions␈αare␈αobserved.␈α The␈αexternal␈αnotation␈αfor␈αsequential␈αprograms␈αis␈αadapted␈αfrom␈αthat␈αof
␈↓ ↓H␈↓Algol 60. We allow as a term an expression of the form
␈↓ ↓H␈↓ ␈↓↓program[<variable list>,<statement list>]␈↓,
␈↓ ↓H␈↓where␈α␈↓↓<variable␈α
list>␈↓␈αis␈α
a␈αlist␈αof␈α
variables␈αlocal␈α
to␈αthe␈α
program,␈αand␈α␈↓↓<statement␈α
list>␈↓␈αis␈α
a␈αlist␈αof␈α
the
␈↓ ↓H␈↓statements␈α
of␈α
the␈αprogram.␈α
As␈α
in␈αAlgol␈α
60,␈α
the␈αstatements␈α
are␈α
separated␈αby␈α
semicolons,␈α
and␈αany
␈↓ ↓H␈↓statement may be preceded by a label followed by a colon.
␈↓ ↓H␈↓ The statements are of the following kinds:
␈↓ ↓H␈↓ 1. Assignment statements of the form
␈↓ ↓H␈↓ ␈↓↓<left hand side> ← <right hand side>␈↓,
␈↓ ↓H␈↓where␈α⊃␈↓↓<left␈α⊃hand␈α⊃side>␈↓␈α⊃is␈α⊃a␈α⊃variable,␈α⊃possibly␈α⊃subscripted,␈α⊃and␈α⊃␈↓↓<right␈α⊃hand␈α⊃side>␈↓␈α⊃is␈α⊃a␈α⊃LISP
␈↓ ↓H␈↓expression that can be evaluated.
␈↓ ↓H␈↓ 2. ␈↓αgo to␈↓ statements of the form
␈↓ ↓H␈↓ ␈↓αgo to␈↓↓ a␈↓
␈↓ ↓H␈↓␈↓ ¬cCHAPTER IV␈↓ 92
␈↓ ↓H␈↓where␈α
␈↓↓a␈↓␈α
is␈α
a␈α
label␈α
or␈α
an␈α
expression␈α
that␈α
evaluates␈α
to␈α
a␈α
label.␈α
Since␈α
labels␈α
are␈α
atoms␈α
in␈αinternal
␈↓ ↓H␈↓notation,␈α
any␈α
expression␈α
evaluating␈α
to␈α
an␈α
atom␈α
may␈αbe␈α
used,␈α
but␈α
the␈α
usual␈α
case␈α
is␈α
a␈αconditional
␈↓ ↓H␈↓expression␈αwherein␈α
the␈αsecond␈α
element␈αof␈α
each␈αpair␈αis␈α
an␈αatom.␈α
Should␈αthe␈α
resulting␈αexpression
␈↓ ↓H␈↓not be an atom or should that atom not be used as a label, an error message will be generated.
␈↓ ↓H␈↓ 3. A conditional statement which has the form
␈↓ ↓H␈↓ ␈↓↓␈↓αif␈↓↓ p1 ␈↓αthen␈↓↓ s1 ␈↓αelse␈↓↓ ␈↓αif␈↓↓ ... ␈↓αelse␈↓↓ ␈↓αif␈↓↓ pn ␈↓αelse␈↓↓ sn␈↓,
␈↓ ↓H␈↓where the ␈↓↓p␈↓'s are propositional expressions having truth values, and the ␈↓↓s␈↓'s are any statements.
␈↓ ↓H␈↓ 4. ␈↓αreturn␈↓↓ e␈↓
␈↓ ↓H␈↓where␈α␈↓↓e␈↓␈αis␈αan␈αarbitrary␈αexpression.␈α The␈α
effect␈αof␈αexecuting␈αthis␈αexpression␈αis␈αto␈αreturn␈α
from␈αthe
␈↓ ↓H␈↓program giving the program as a term the value of the expression ␈↓↓e␈↓.
␈↓ ↓H␈↓ As an example, we might write ␈↓↓reverse␈↓ as follows:
␈↓ ↓H␈↓ ␈↓↓reverse u ← ␈↓αprogram␈↓↓[[v];
␈↓ ↓H␈↓↓ v ← ␈↓¬NIL␈↓↓;
␈↓ ↓H␈↓↓ a: ␈↓αif␈↓↓ ␈↓αn␈↓↓␈α∧u ␈↓αthen␈↓↓ ␈↓αreturn␈↓↓ v;
␈↓ ↓H␈↓↓ v ← ␈↓αa␈↓↓␈α∧u . v;
␈↓ ↓H␈↓↓ u ← ␈↓αd␈↓↓␈α∧v;
␈↓ ↓H␈↓↓ ␈↓αgo to␈↓ a].
␈↓ ↓H␈↓ The internal form of the same program is
␈↓ ↓H␈↓ (DE REVERSE (U) (PROG (V)
␈↓ ↓H␈↓ (SETQ V NIL)
␈↓ ↓H␈↓ A
␈↓ ↓H␈↓ (COND ((NULL U) (RETURN V)))
␈↓ ↓H␈↓ (SETQ V (CONS (CAR U) V))
␈↓ ↓H␈↓ (SETQ U (CDR U))
␈↓ ↓H␈↓ (GO A)
␈↓ ↓H␈↓ ))
␈↓ ↓H␈↓where␈αthe␈αparagraphing␈αis␈αonly␈αfor␈αthe␈αreader's␈αconvenience.␈α Notice␈αthat␈αin␈αinternal␈αform,␈αlabels
␈↓ ↓H␈↓are statements rather than attachments to statements.
␈↓ ↓H␈↓ Here are some ways we might write ␈↓↓append␈↓:
␈↓ ↓H␈↓ ␈↓↓u * v ← ␈↓αprogram␈↓↓[
␈↓ ↓H␈↓↓ ␈↓αreturn␈↓↓ ␈↓αif␈↓↓ ␈↓αn␈↓↓␈α∧u ␈↓αthen␈↓↓ v ␈↓αelse␈↓↓ ␈↓αa␈↓↓␈α∧u . [␈↓αd␈↓↓␈α∧u * v]]␈↓,
␈↓ ↓H␈↓is just a trivial rewrite of the recursive definition.
␈↓ ↓H␈↓ ␈↓↓u * v ← ␈↓αprog␈↓↓ram[w;
␈↓ ↓H␈↓␈↓ ¬cCHAPTER IV␈↓ 93
␈↓ ↓H␈↓↓ ␈↓αif␈↓↓ ␈↓αn␈↓↓␈α∧u ␈↓αthen␈↓↓ ␈↓αreturn␈↓↓ v;
␈↓ ↓H␈↓↓ w ← ␈↓αa␈↓↓␈α∧u . [␈↓αd␈↓↓␈α∧u * v];
␈↓ ↓H␈↓↓ ␈↓αreturn␈↓↓ w]␈↓
␈↓ ↓H␈↓is␈αalmost␈α
as␈αclose␈α
to␈αthe␈α
pure␈αLISP␈α
form.␈α If␈αwe␈α
want␈αto␈α
replace␈αthe␈α
recursion␈αby␈α
a␈αloop,␈α
we␈αcan
␈↓ ↓H␈↓write
␈↓ ↓H␈↓ ␈↓↓u * v ← ␈↓αprog␈↓↓ram[w, u1, v1;
␈↓ ↓H␈↓↓ w ← ␈↓¬NIL␈↓↓;
␈↓ ↓H␈↓↓ u1 ← u;
␈↓ ↓H␈↓↓ v1 ← v;
␈↓ ↓H␈↓↓ a: ␈↓αif␈↓↓ ␈↓αn␈↓↓␈α∧u1 ␈↓αthen␈↓↓ ␈↓αgo to* b;
␈↓ ↓H␈↓α w ← a␈α∧u1 . w;
␈↓ ↓H␈↓α u1 ← d␈α∧u;
␈↓ ↓H␈↓α go to* a;
␈↓ ↓H␈↓α b: if n␈α∧w then return v1;
␈↓ ↓H␈↓α v1 ← a␈α∧w . v1;
␈↓ ↓H␈↓α ␈↓πT␈↓α ← d␈α∧w;
␈↓ ↓H␈↓α go to* b]␈↓.
␈↓ ↓H␈↓This corresponds to the recursive program
␈↓ ↓H␈↓ ␈↓↓u * v ← app[u,v,␈↓¬NIL␈↓↓]
␈↓ ↓H␈↓↓ app[u,v,w] ← ␈↓αif␈↓↓ ␈↓αn␈↓↓␈α∧u ␈↓αthen␈↓↓ [␈↓αif␈↓↓ ␈↓αn␈↓↓␈α∧w ␈↓αthen␈↓↓ v ␈↓αelse␈↓↓ app[u,␈↓αa␈↓↓␈α∧w . v,␈↓αd␈↓↓␈α∧w]]
␈↓ ↓H␈↓↓␈↓αelse␈↓↓ app[␈↓αd␈↓↓␈α∧u,v,␈↓αa␈↓↓␈α∧u . w]␈↓
␈↓ ↓H␈↓which can save some storage if it is compiled or interpreted without using the stack.
␈↓ ↓H␈↓ We␈αshall␈α
not␈αtreat␈αthe␈α
mathematics␈αof␈αsequential␈α
programs␈αfully␈αat␈α
this␈αpoint.␈α
However,␈αa
␈↓ ↓H␈↓sequential␈α∂program␈α∞that␈α∂occurs␈α∂as␈α∞a␈α∂term␈α∞can␈α∂be␈α∂replaced␈α∞by␈α∂a␈α∞term␈α∂involving␈α∂only␈α∞functional
␈↓ ↓H␈↓programs provided the following conditions are observed:
␈↓ ↓H␈↓ 1.␈αAll␈α
variables␈αlocal␈α
to␈αthe␈αprogram␈α
are␈αinitialized␈α
before␈αbeing␈αused.␈α
Of␈αcourse,␈α
it␈αcould
␈↓ ↓H␈↓be␈αtaken␈α
as␈αa␈αconvention␈α
that␈αthese␈α
variables␈αare␈αinitialized␈α
to␈α␈↓¬NIL␈↓␈αwhen␈α
the␈αprogram␈α
is␈αentered.
␈↓ ↓H␈↓Then␈αit␈αwouldn't␈αaffect␈αthe␈αcorrectness␈αof␈αthe␈αtranslation␈αto␈αa␈αfunctional␈αprogram␈αif␈αsome␈αof␈αthem
␈↓ ↓H␈↓weren't further initialized.
␈↓ ↓H␈↓ 2. All assignments are to variables local to the program.
␈↓ ↓H␈↓ A␈α
new␈αfunction␈α
definition␈α
is␈αmade␈α
for␈α
each␈αbranch␈α
(i.e.␈α
conditional␈α␈↓αgo to␈↓)␈α
in␈α
the␈αoriginal
␈↓ ↓H␈↓program.␈α The␈αargument␈α
of␈αthe␈αfunction␈αis␈α
a␈αlist␈αwhose␈αelements␈α
are␈αvalues␈αassigned␈αto␈α
the␈αlocal
␈↓ ↓H␈↓variables,␈αi.e.␈α
the␈αlist␈α
has␈αas␈α
many␈αelements␈α
as␈αthere␈α
are␈αlocal␈α
variables.␈α The␈α
value␈αof␈αthe␈α
function
␈↓ ↓H␈↓is␈α
the␈αvalue␈α
that␈αwill␈α
be␈α
␈↓αreturn␈↓ed␈αfrom␈α
the␈αprogram␈α
given␈α
that␈αthe␈α
local␈αvariables␈α
have␈αthe␈α
values
␈↓ ↓H␈↓given␈αin␈αthe␈α
argument␈αwhen␈αthe␈αbranch␈α
is␈αreached.␈α The␈α␈↓αprogram␈↓␈α
expression␈αitself␈αis␈αreplaced␈α
by
␈↓ ↓H␈↓␈↓ ¬cCHAPTER IV␈↓ 94
␈↓ ↓H␈↓an␈α
application␈α∞of␈α
the␈α∞function␈α
corresponding␈α∞to␈α
the␈α
first␈α∞branch␈α
encountered␈α∞in␈α
the␈α∞program␈α
to
␈↓ ↓H␈↓the␈α∂state␈α∞vector␈α∂whose␈α∞components␈α∂have␈α∞the␈α∂values␈α∞they␈α∂will␈α∞have␈α∂the␈α∞first␈α∂time␈α∞the␈α∂branch␈α∞is
␈↓ ↓H␈↓reached written as functions of the external variables.
␈↓ ↓H␈↓ As␈αan␈αexample,␈αconsider␈αthe␈αfollowing␈αexpression␈αthat␈αgives␈αthe␈αresult␈αof␈αappending␈αthe␈αlist
␈↓ ↓H␈↓␈↓↓a␈↓ with the reversal of ␈↓↓a*b␈↓:
␈↓ ↓H␈↓ ␈↓↓a␈α*␈α␈↓αprogram␈↓↓[[u,v]␈αu␈α←␈αa␈α*␈αb;␈αv␈α←␈α␈↓¬NIL␈↓↓;␈αloop:␈α␈↓αif␈↓↓␈α␈↓αn␈↓↓␈α∧u␈α␈↓αthen␈↓↓␈α␈↓αreturn␈↓↓␈αv;␈αv␈α←␈α␈↓αa␈↓↓␈α∧u␈α.␈αv;␈αu␈α←␈α␈↓αd␈↓↓␈α∧u;␈α␈↓αgo to*
␈↓ ↓H␈↓αloop]␈↓.
␈↓ ↓H␈↓This expression can be replaced by
␈↓ ↓H␈↓ ␈↓↓a * loop <u, ␈↓¬NIL␈↓↓>␈↓
␈↓ ↓H␈↓and the recursive definition
␈↓ ↓H␈↓ ␈↓↓loop z ← ␈↓αif␈↓↓ ␈↓αn␈↓↓␈α∧␈↓αa␈↓↓␈α∧z ␈↓αthen␈↓↓ ␈↓αad␈↓↓␈α∧z ␈↓αelse␈↓↓ loop <␈↓αda␈↓↓␈α∧z, ␈↓αaa␈↓↓␈α∧z . ␈↓αad␈↓↓␈α∧z>␈↓.
␈↓ ↓H␈↓ Should␈α
a␈α
program␈αmake␈α
assignments␈α
to␈α
external␈αvariables,␈α
an␈α
ambiguity␈α
arises.␈α Suppose␈α
we
␈↓ ↓H␈↓evaluate the expression
␈↓ ↓H␈↓ ␈↓↓<x, ␈↓αprogram␈↓↓[[] x ← ␈↓αd␈↓↓␈α∧x], x>␈↓.
␈↓ ↓H␈↓when␈α␈↓↓x␈↓␈αhas␈αthe␈αvalue␈α(A␈αB).␈α If␈αthe␈αarguments␈αof␈αthe␈αlist␈αare␈α"executed"␈αin␈αright␈αto␈αleft␈αorder,␈αthe
␈↓ ↓H␈↓expression␈α
will␈αhave␈α
value␈α
((A␈αB)␈α
(B)␈α(B)),␈α
whereas␈α
if␈αthe␈α
execution␈αis␈α
from␈α
right␈αto␈α
left,␈αthe␈α
value
␈↓ ↓H␈↓will␈αbe␈α
((B)␈α(B)␈α
(A␈αB)).␈α
However,␈αthe␈αmathematical␈α
semantics␈αof␈α
expressions␈αdon't␈α
prescribe␈αany
␈↓ ↓H␈↓order␈α
of␈αevaluation,␈α
and␈α
experience␈αwith␈α
ALGOL␈α
60,␈αwhich␈α
prescribed␈α
left-to-right␈αevaluation␈α
in
␈↓ ↓H␈↓order␈α
to␈α
give␈α
a␈αdefinite␈α
meaning␈α
to␈α
function␈α
procedures␈αthat␈α
alter␈α
external␈α
variables,␈α
has␈αshown
␈↓ ↓H␈↓that the quality of compiled code is greatly reduced by prescribing a fixed order.
␈↓ ↓H␈↓ This␈α
ambiguity␈αcan␈α
be␈α
resolved␈αby␈α
rewriting␈α
expressions␈αcontaining␈α
programs␈α
that␈αchange
␈↓ ↓H␈↓variables␈α
in␈α
the␈α
expression␈α
using␈α
lambda␈αexpressions␈α
to␈α
force␈α
a␈α
desired␈α
order␈α
of␈αevaluation.␈α
Thus
␈↓ ↓H␈↓the above expression could be written
␈↓ ↓H␈↓ ␈↓↓[λy:[λz:<z,y,y>][␈↓αprogram␈↓↓[[] x ← ␈↓αd␈↓↓␈α∧x]]][x]␈↓
␈↓ ↓H␈↓which␈α⊂would␈α⊂evaluate␈α⊂to␈α⊂((B)␈α⊂(A␈α⊂B)␈α⊂(A␈α⊂B))␈α⊂in␈α⊂the␈α⊂above␈α⊂case.␈α⊂ Seven␈α⊂other␈α⊂results␈α⊃could␈α⊂be
␈↓ ↓H␈↓obtained␈α
by␈α
putting␈α
different␈α
combinations␈α
of␈α∞␈↓↓z␈↓␈α
and␈α
␈↓↓y␈↓␈α
between␈α
the␈α
pointy␈α
brackets.␈α∞ Once␈α
these
␈↓ ↓H␈↓ambiguities␈α
have␈α
been␈α
resolved,␈α
it␈α
would␈α
seem␈α
that␈α
we␈α
could␈α
translate␈α
an␈α
outer␈α
sequential␈α
program
␈↓ ↓H␈↓containing␈αinner␈αsequential␈αprograms␈αinto␈αa␈αfunction␈αprogram␈αin␈αa␈αunique␈αway␈αeven␈αallowing␈αthe
␈↓ ↓H␈↓inner␈αprograms␈αto␈αmake␈αassignments␈αto␈αvariables␈αin␈αthe␈αouter␈αprograms.␈α The␈αrules␈αfor␈αdoing␈α
this
␈↓ ↓H␈↓haven't been worked out, however.
␈↓ ↓H␈↓ An␈α∪assignment␈α∪may␈α∪be␈α∩regarded␈α∪as␈α∪an␈α∪␈↓αprogram␈↓␈α∩expression.␈α∪ Thus␈α∪␈↓↓[x ← qa y].z␈↓␈α∪is␈α∩an
␈↓ ↓H␈↓abbreviation for ␈↓αprogram␈↓↓[[]x ← y].z␈↓.
␈↓ ↓H␈↓Exercises:
␈↓ ↓H␈↓␈↓ ¬cCHAPTER IV␈↓ 95
␈↓ ↓H␈↓ 1.␈α
Write␈α
a␈α
LISP␈α
predicate␈α
that␈α
will␈α
determine␈α
whether␈α
a␈α
PROG␈α
in␈α
internal␈α∞form␈α
satisfies
␈↓ ↓H␈↓the above conditions for replacement by a functional term.
␈↓ ↓H␈↓ 2.␈α⊃Given␈α⊃that␈α⊃a␈α∩PROG␈α⊃satisfies␈α⊃the␈α⊃conditions,␈α⊃write␈α∩a␈α⊃LISP␈α⊃functions␈α⊃to␈α∩convert␈α⊃the
␈↓ ↓H␈↓PROG expression and give the a list of the required auxiliary function definitions.
␈↓ ↓H␈↓ The␈αreason␈α
for␈αdiscussing␈αhow␈α
to␈αrewrite␈αthe␈α
sequential␈αprogram␈αas␈α
a␈αfunctional␈αprogram␈α
is
␈↓ ↓H␈↓to␈αapply␈αthe␈αthe␈αtheory␈αof␈αchapter␈α3␈α
to␈αthe␈αsequential␈αcase.␈α The␈αabove␈αconditions␈αpermit␈αa␈α
purely
␈↓ ↓H␈↓local␈α∞rewrite,␈α∞but␈α∞it␈α∞seems␈α∞evident␈α∞that␈α∞if␈α∞an␈α∞outer␈α∞sequential␈α∞program␈α∞containing␈α∞an␈α∂inner␈α∞one
␈↓ ↓H␈↓satisfies␈α
the␈α
initialization␈α∞and␈α
local␈α
assignment␈α
(i.e.␈α∞ no␈α
side-effect)␈α
conditions,␈α
then␈α∞the␈α
program
␈↓ ↓H␈↓can␈αbe␈αconverted␈αto␈αfunctional␈αform␈αeven␈αif␈αit␈αcontains␈αsequential␈αsubprograms␈αthat␈αviolate␈αthese
␈↓ ↓H␈↓conditions␈α⊂provided␈α⊃that␈α⊂all␈α⊃assignments␈α⊂in␈α⊂the␈α⊃inner␈α⊂program␈α⊃are␈α⊂at␈α⊂least␈α⊃local␈α⊂to␈α⊃the␈α⊂outer
␈↓ ↓H␈↓program. The rules for doing this have not been formulated as yet.
␈↓ ↓H␈↓ There␈α⊂are␈α⊂three␈α⊂circumstances␈α⊂in␈α∂which␈α⊂sequential␈α⊂programs␈α⊂are␈α⊂preferred␈α⊂to␈α∂functional
␈↓ ↓H␈↓programs:
␈↓ ↓H␈↓ 1.␈αIn␈αsome␈αcases␈αand␈αfor␈αsome␈αpeople,␈αit␈αis␈αeasier␈αto␈αthink␈αabout␈αhow␈αto␈αgo␈αfrom␈αthe␈αinitial
␈↓ ↓H␈↓conditions␈α
step-by-step␈α
to␈α
the␈α
final␈α
result␈α
than␈α
to␈α
think␈α
about␈α
how␈α
the␈α
final␈α
result␈α
can␈αbe␈α
obtained
␈↓ ↓H␈↓from␈α∩easier␈α∩cases.␈α∩ There␈α∩seems␈α∩to␈α∩be␈α∩a␈α∩matter␈α∩of␈α∩taste␈α∩to␈α∩a␈α∩substantial␈α∩extent,␈α∪though␈α∩the
␈↓ ↓H␈↓functional form seems to have clear conceptual advantages for functions like ␈↓↓append␈↓ and ␈↓↓subst␈↓.
␈↓ ↓H␈↓ 2.␈αWhen␈αthere␈αare␈αa␈αlarge␈αnumber␈αof␈αvariables,␈αit␈αcan␈αturn␈αout␈αthat␈αthe␈αnecessary␈αfunctions
␈↓ ↓H␈↓have an unwieldy number of arguments.
␈↓ ↓H␈↓ 3.␈α⊃When␈α∩we␈α⊃are␈α∩considering␈α⊃a␈α∩program␈α⊃that␈α∩interacts␈α⊃with␈α∩an␈α⊃environment␈α∩instead␈α⊃of
␈↓ ↓H␈↓producing an answer, the sequential form may be required, although this hasn't been proved.
␈↓ ↓H␈↓Remarks:
␈↓ ↓H␈↓ 1.␈αBesides␈α(SETQ␈αvar␈αexp),␈αmost␈αLISPs␈αallow␈α(SET␈αexp1␈αexp2),␈αwhere␈α␈↓↓exp1␈↓␈αis␈αevaluated␈αto
␈↓ ↓H␈↓determine␈αto␈αwhat␈αvariable␈αthe␈αassignment␈αis␈αto␈αbe␈αmade.␈α If␈α␈↓↓exp1␈↓␈αdoesn't␈αevaluate␈αto␈αa␈αvariable,
␈↓ ↓H␈↓an error is signalled.
␈↓ ↓H␈↓ 2. LISP admits arrays.
␈↓ ↓H␈↓2. ␈↓αPseudo-functions that modify list structures␈↓
␈↓ ↓H␈↓ In␈α⊃pure␈α∩LISP,␈α⊃list␈α⊃structure␈α∩is␈α⊃never␈α⊃changed.␈α∩ ␈↓↓car␈↓␈α⊃and␈α⊃␈↓↓cdr␈↓␈α∩merely␈α⊃move␈α⊃about␈α∩in␈α⊃list
␈↓ ↓H␈↓structure,␈αand␈α␈↓↓cons␈↓␈αcreates␈αnew␈αlist␈αstructure␈α
from␈αthe␈αfree␈αstorage␈αlist.␈α Of␈αcourse,␈αa␈α
variable␈αcan
␈↓ ↓H␈↓get␈αa␈αnew␈α
value␈αthat␈αcorresponds,␈αfor␈α
instance,␈αto␈αputting␈αan␈α
element␈αon␈αthe␈αend␈α
of␈αa␈αlist,␈α
but␈αin
␈↓ ↓H␈↓pure␈α∞LISP␈α
this␈α∞can␈α
only␈α∞be␈α
accomplished␈α∞by␈α∞creating␈α
new␈α∞list␈α
structure.␈α∞ In␈α
this␈α∞section␈α∞we␈α
will
␈↓ ↓H␈↓␈↓ ¬cCHAPTER IV␈↓ 96
␈↓ ↓H␈↓discuss␈αoperations␈αthat␈αactually␈αmodify␈αlist␈αstructure.␈α They␈αoften␈αhave␈αefficiency␈α
advantages,␈αbut
␈↓ ↓H␈↓there␈α
use␈α
interferes␈αwith␈α
saving␈α
memory␈αby␈α
using␈α
merging␈αlist␈α
structure,␈α
and␈αit␈α
is␈α
techniques␈αfor
␈↓ ↓H␈↓proving correctness of such programs are not well developed.
␈↓ ↓H␈↓ The␈α∀simplest␈α∀way␈α∀to␈α∀express␈α∀operations␈α∀that␈α∀modify␈α∀list␈α∀structure␈α∀is␈α∀in␈α∀the␈α∀form␈α∪of
␈↓ ↓H␈↓assignments to ␈↓↓car-cdr␈↓ chains of variables, e.g. we may write
␈↓ ↓H␈↓ ␈↓↓␈↓αada␈↓↓␈α∧x ← y.z␈↓.
␈↓ ↓H␈↓The␈α
effect␈αof␈α
executing␈α
this␈αstatement␈α
is␈αto␈α
replace␈α
the␈α␈↓αada␈↓␈α∧part␈α
of␈αthe␈α
list␈α
structure␈αpointed␈α
to␈αby␈α
␈↓↓x␈↓
␈↓ ↓H␈↓with␈αthe␈αvalue␈αof␈αthe␈α
right␈αhand␈αside.␈α As␈αan␈α
expression,␈αthe␈αstatement␈αtakes␈αthe␈α
value␈αassigned.
␈↓ ↓H␈↓In␈α∞internal␈α∞notation,␈α∂we␈α∞use␈α∞the␈α∂pseudo-functions␈α∞(RPLACA X Y)␈α∞and␈α∂(RPLACD X Y)␈α∞which
␈↓ ↓H␈↓correspond to the statements
␈↓ ↓H␈↓ ␈↓↓␈↓αa␈↓↓␈α∧x ← y␈↓
␈↓ ↓H␈↓and
␈↓ ↓H␈↓ ␈↓↓␈↓αd␈↓↓␈α∧x ← y␈↓
␈↓ ↓H␈↓respectively.
␈↓ ↓H␈↓ RPLACA␈αand␈αRPLACD␈αare␈αhighly␈αunclean.␈α Thus␈αthe␈αeffect␈αof␈αevaluating␈α
an␈αexpression
␈↓ ↓H␈↓involving␈αRPLACA␈αor␈αRPLACD␈αdepends␈αon␈αthe␈αstate␈αof␈αlist␈αstructure␈αand␈αnot␈αmerely␈αon␈αthe␈αS-
␈↓ ↓H␈↓expressions␈α
the␈α
variables␈α
have␈α
as␈α
values.␈α
Suppose,␈αfor␈α
example,␈α
that␈α
the␈α
variables␈α
␈↓↓x1␈↓␈α
and␈α␈↓↓x2␈↓␈α
each
␈↓ ↓H␈↓have␈αthe␈α
value␈α(A␈αB),␈α
and␈αconsider␈αthe␈α
effect␈αof␈α(SETQ␈α
Z␈α(RPLACA␈α(CDR␈α
X)␈αC)).␈α Z␈α
gets␈αthe
␈↓ ↓H␈↓value␈α
(C),␈α
and␈α
X␈α
gets␈α
the␈α
values␈α
(A␈α
C),␈α
but␈αthe␈α
new␈α
value␈α
of␈α
Y␈α
depends␈α
on␈α
whether␈α
its␈α
copy␈αof␈α
(A
␈↓ ↓H␈↓B)␈α
is␈α
the␈α
same␈α
list␈α
structure␈α
as␈α
X's␈α
copy.␈α
If␈αyes,␈α
the␈α
new␈α
value␈α
of␈α
Y␈α
is␈α
also␈α
(A␈α
C);␈α
otherwise␈αits
␈↓ ↓H␈↓value remains (A B).
␈↓ ↓H␈↓ The␈α⊂uncleanliness␈α⊃of␈α⊂RPLACA␈α⊂and␈α⊃RPLACD␈α⊂means␈α⊂that␈α⊃the␈α⊂programmer␈α⊃must␈α⊂know
␈↓ ↓H␈↓exactly what list structures merge. A typical application is the pseudo-function ␈↓↓nconc␈↓ defined by
␈↓ ↓H␈↓ ␈↓↓nconc[u,v] ← ␈↓αprog␈↓↓ram[[w];
␈↓ ↓H␈↓↓ ␈↓αn␈↓↓␈α∧u ← ␈↓αreturn␈↓↓ v;
␈↓ ↓H␈↓↓ w ← u;
␈↓ ↓H␈↓↓loop: ␈↓αif␈↓↓ ␈↓αn␈↓↓␈α∧␈↓αd␈↓↓␈α∧w ␈↓αthen␈↓↓ qbegin ␈↓αd␈↓↓␈α∧w ← v; ␈↓αreturn␈↓↓ u qend;
␈↓ ↓H␈↓↓ w ← ␈↓αd␈↓↓␈α∧w;
␈↓ ↓H␈↓↓ ␈↓αgo␈↓↓ loop]␈↓.
␈↓ ↓H␈↓␈↓↓nconc␈↓ can also be given a definition that has the form of a recursive program, namely
␈↓ ↓H␈↓ ␈↓↓nconc[u,v] ← nconc1[u,u,v]␈↓
␈↓ ↓H␈↓with
␈↓ ↓H␈↓ ␈↓↓nconc[u,w,v] ← ␈↓αif␈↓↓ ␈↓αn␈↓↓␈α∧w ␈↓αthen␈↓↓ v ␈↓αelse␈↓↓ ␈↓αif␈↓↓ ␈↓αn␈↓↓␈α∧␈↓αd␈↓↓␈α∧w ␈↓αthen␈↓↓ [λz:u][rplacd[w,v]] ␈↓αelse␈↓↓ nconc[u, ␈↓αd␈↓↓␈α∧w, v]␈↓.
␈↓ ↓H␈↓␈↓ ¬cCHAPTER IV␈↓ 97
␈↓ ↓H␈↓ The␈α⊃value␈α⊃of␈α⊂␈↓↓nconc[u,v]␈↓␈α⊃is␈α⊃just␈α⊂␈↓↓u*v,␈↓␈α⊃but␈α⊃it␈α⊂achieves␈α⊃this␈α⊃result␈α⊂by␈α⊃modifying␈α⊃the␈α⊂last
␈↓ ↓H␈↓element␈αof␈α␈↓↓u␈↓␈αto␈αpoint␈αto␈α␈↓↓v.␈↓␈α It␈αis␈αtypically␈αused␈αwhen␈αno␈αother␈αvariable␈αpoints␈αto␈αlist␈αstructure␈α
that
␈↓ ↓H␈↓merges␈α
into␈α␈↓↓u,␈↓␈α
and␈αthe␈α
old␈α
value␈αof␈α
␈↓↓u␈↓␈αwill␈α
not␈αbe␈α
used␈α
again.␈α In␈α
that␈αcase,␈α
␈↓↓nconc␈↓␈αis␈α
advantageous,
␈↓ ↓H␈↓because␈α
it␈α
does␈αno␈α
␈↓↓cons␈↓es,␈α
and␈α
thus␈αcan't␈α
initiate␈α
garbage␈α
collection.␈α No␈α
formal␈α
methods␈α
exist␈αat
␈↓ ↓H␈↓present for proving that these conditions are met.
␈↓ ↓H␈↓ RPLACD␈α∂can␈α∂also␈α∂be␈α∂used␈α∂to␈α∂insert␈α∂an␈α∂element␈α∂into␈α∂the␈α∂middle␈α∂of␈α∂a␈α∂list.␈α⊂ Suppose,␈α∂for
␈↓ ↓H␈↓example,␈αthat␈αwe␈αwish␈αto␈αinsert␈αthe␈αatom␈αB␈αafter␈αevery␈αoccurrence␈αof␈αthe␈αatom␈αA␈αin␈αa␈αlist␈α␈↓↓u.␈↓␈α We
␈↓ ↓H␈↓can␈αdefine␈αa␈αpure␈α
LISP␈αfunction␈αthat␈αgives␈αa␈α
list␈αobtained␈αfrom␈αthe␈αlist␈α
␈↓↓u␈↓␈αby␈αinserting␈αsuch␈αB's␈α
as
␈↓ ↓H␈↓follows:
␈↓ ↓H␈↓ ␈↓↓insertb u ← ␈↓αif␈↓↓ ␈↓αn␈↓↓␈α∧u ␈↓αthen␈↓↓ ␈↓¬NIL␈↓↓ ␈↓αelse␈↓↓ ␈↓αif␈↓↓ ␈↓αa␈↓↓␈α∧u = A ␈↓αthen␈↓↓ A.[B.insertb ␈↓αd␈↓↓␈α∧u] ␈↓αelse␈↓↓ ␈↓αa␈↓↓␈α∧u . insertb ␈↓αd␈↓↓␈α∧u␈↓.
␈↓ ↓H␈↓Computing␈α␈↓↓insertb␈αu␈↓␈αdoes␈αnot␈αchange␈αthe␈αvalue␈αof␈α␈↓↓u,␈↓␈αbecause␈αnew␈αlist␈αstructure␈αis␈αmanufactured.
␈↓ ↓H␈↓On the other hand, if we define
␈↓ ↓H␈↓ ␈↓↓insertb2 u ← ␈↓αprog␈↓↓ram[[w];
␈↓ ↓H␈↓↓ w ← u;
␈↓ ↓H␈↓↓loop: ␈↓αif␈↓↓ ␈↓αn␈↓↓␈α∧w ␈↓αthen␈↓↓ ␈↓αreturn␈↓↓ u;
␈↓ ↓H␈↓↓ ␈↓αif␈↓↓ ␈↓αa␈↓↓␈α∧w = A ␈↓αthen␈↓↓ ␈↓αd␈↓↓␈α∧w ← B . ␈↓αd␈↓↓␈α∧w;
␈↓ ↓H␈↓↓ w ← ␈↓αd␈↓↓␈α∧w;
␈↓ ↓H␈↓↓ ␈↓αgo␈↓↓ loop]␈↓,
␈↓ ↓H␈↓we␈αget␈α
a␈αprogram␈α
that␈αdoes␈α
the␈αactual␈α
insertions.␈α It␈αis␈α
faster,␈αbecause␈α
it␈αuses␈α
fewer␈α␈↓↓cons␈↓es,␈α
but␈αit
␈↓ ↓H␈↓will␈α⊂damage␈α⊂any␈α⊂list␈α∂structure␈α⊂that␈α⊂merges␈α⊂with␈α⊂that␈α∂representing␈α⊂␈↓↓u,␈↓␈α⊂and␈α⊂it␈α⊂is␈α∂mathematically
␈↓ ↓H␈↓recalcitrant.
␈↓ ↓H␈↓3. ␈↓αRE-ENTRANT LIST STRUCTURE␈↓
␈↓ ↓H␈↓ So␈α
far␈αwe␈α
have␈α
only␈αconsidered␈α
list␈α
structure␈αin␈α
which␈α
all␈α␈↓↓car-cdr␈↓␈α
chains␈α
terminate␈αin␈α
atoms.
␈↓ ↓H␈↓Mathematically␈αinfinite␈αlist␈αstructures␈αare␈αalso␈αpossible.␈α They␈αcan't␈αbe␈αrepresented␈αin␈αa␈αcomputer,
␈↓ ↓H␈↓but␈αsince␈αthey␈αcan␈αsatisfy␈αthe␈αLISP␈αalgebraic␈αaxioms,␈αwe␈αhave␈αhad␈αto␈αexclude␈αthem␈αin␈αour␈αproofs
␈↓ ↓H␈↓by␈α
axiom␈α
schemata␈α
of␈αinduction.␈α
Another␈α
possibility␈α
is␈α
the␈αre-entrant␈α
list␈α
structure.␈α
These␈αcan␈α
be
␈↓ ↓H␈↓created␈αby␈αthe␈αRPLACA␈αand␈αRPLACD␈αoperations.␈α For␈αexample,␈αif␈αthe␈αvariable␈α␈↓↓x␈↓␈αhas␈αvalue␈α(A
␈↓ ↓H␈↓B), executing the statement
␈↓ ↓H␈↓ ␈↓↓␈↓αa␈↓↓␈α∧x ← x␈↓
␈↓ ↓H␈↓gives rise to a circular structure like that of figure 1a. If we then execute
␈↓ ↓H␈↓ ␈↓↓␈↓αd␈↓↓␈α∧x ← x␈↓
␈↓ ↓H␈↓we␈α∞get␈α∞the␈α
doubly␈α∞re-entrant␈α∞structure␈α∞of␈α
figure␈α∞1b.␈α∞ Other␈α∞possibilities␈α
are␈α∞shown␈α∞in␈α∞the␈α
other
␈↓ ↓H␈↓parts of figure 1.
␈↓ ↓H␈↓␈↓ ¬cCHAPTER IV␈↓ 98
␈↓ ↓H␈↓ Re-entrant␈αlist␈αstructures␈αdo␈αnot␈αcorrespond␈α
to␈αS-expressions,␈αand␈αthe␈αcorrectness␈αof␈αmost␈α
of
␈↓ ↓H␈↓programs␈α
given␈α
in␈α
this␈α
book␈α
depends␈α
on␈α
the␈α
data␈α
being␈α
non-re-entrant.␈α
Re-entrant␈α
structures␈α
can
␈↓ ↓H␈↓be␈α⊂represented␈α⊂by␈α⊃S-expressions␈α⊂provided␈α⊂certain␈α⊃atoms␈α⊂are␈α⊂reserved␈α⊂for␈α⊃use␈α⊂as␈α⊂labels␈α⊃and␈α⊂a
␈↓ ↓H␈↓suitable␈αconvention␈α
is␈αadopted␈αfor␈α
distinguishing␈αordinary␈α
atoms␈αfrom␈αlabels␈α
and␈αpointers␈α
to␈αthe
␈↓ ↓H␈↓labels.␈α∞ For␈α∞example,␈α∞the␈α
structure␈α∞of␈α∞figure␈α∞1b␈α
might␈α∞be␈α∞represented␈α∞by␈α∞((LABEL␈α
A).((POINT
␈↓ ↓H␈↓A).(POINT␈αA))).␈α Programs␈αthat␈αcompute␈αwith␈αre-entrant␈αstructures␈αneed␈αto␈αkeep␈αlists␈αof␈αvertices
␈↓ ↓H␈↓they␈αhave␈αvisited␈αso␈αthat␈αthey␈αcan␈αtell␈αwhen␈αthey␈αare␈αabout␈αto␈αre-enter.␈α Thus␈αthe␈αequivalence␈αof
␈↓ ↓H␈↓merging list structure can be tested by the predicate
␈↓ ↓H␈↓ ␈↓↓equiv[x,y] ← equiv1[x,y,␈↓¬NIL␈↓↓] ≠ LOSE␈↓
␈↓ ↓H␈↓where
␈↓ ↓H␈↓ ␈↓↓equiv1[x,y,u]␈α∩←␈α∩␈↓αif␈↓↓␈α∩x␈α∩␈↓αeq␈↓↓␈α∩y␈α∩∨␈α∩match[x,y,u]␈α∩␈↓αthen␈↓↓␈α∩u␈α∩␈↓αelse␈↓↓␈α∩␈↓αif␈↓↓␈α∩u␈α∩=␈α∩LOSE␈α∩∨␈α∩␈↓αat␈↓↓␈αεx␈α∩∨␈α∩␈↓αat␈↓↓␈αεy␈α⊃∨
␈↓ ↓H␈↓↓unmatch[x,y,u] ␈↓αthen␈↓↓ LOSE ␈↓αelse␈↓↓ equiv1[␈↓αd␈↓↓␈α∧x,␈↓αd␈↓↓␈α∧y,equiv1[␈↓αa␈↓↓␈α∧x,␈↓αa␈↓↓␈α∧y,[x.y].u]]␈↓,
␈↓ ↓H␈↓ ␈↓↓match[x,y,u] ← ¬␈↓αn␈↓↓␈α∧u ∧ [x.y ␈↓αeq␈↓↓ual ␈↓αa␈↓↓␈α∧u ∨ match[x,y,␈↓αd␈↓↓␈α∧u]]␈↓,
␈↓ ↓H␈↓and
␈↓ ↓H␈↓ ␈↓↓unmatch[x,y,u] ← ¬␈↓αn␈↓↓␈α∧u ∧ [x = ␈↓αaa␈↓↓␈α∧u ∨ y = ␈↓αda␈↓↓␈α∧u ∨ unmatch[x,y,␈↓αd␈↓↓␈α∧u]]␈↓.
␈↓ ↓H␈↓EXERCISES
␈↓ ↓H␈↓ #. Write a program to list the atoms in a possibly re-entrant list structure.
␈↓ ↓H␈↓ #.␈αWrite␈αa␈αprogram␈α
to␈αtranslate␈αa␈αgraph␈α
description␈αfrom␈αthe␈αnotation␈α
of␈αChapter␈α1␈αto␈αa␈α
re-
␈↓ ↓H␈↓entrant list structure.
␈↓ ↓H␈↓ #.␈α
Write␈αfunctions␈α
to␈αtranslate␈α
in␈α
each␈αdirection␈α
between␈αpossibly␈α
re-entrant␈α
structures␈αand
␈↓ ↓H␈↓the S-expressions corresponding to them using the LABEL, POINTER notation described above.
␈↓ ↓H␈↓ #.␈α
Write␈α
an␈α∞axiom␈α
schema␈α
of␈α∞induction␈α
for␈α
finite␈α∞possibly␈α
re-entrant␈α
list␈α∞structures.␈α
Hint:
␈↓ ↓H␈↓The␈αschema␈α
can␈αbe␈αbaased␈α
on␈αan␈αassertion␈α
of␈αconvergence␈αof␈α
a␈αprogram␈αthat␈α
scans␈αa␈αlist␈α
structure
␈↓ ↓H␈↓keeping track of the vertices it has alread visited.
␈↓ ↓H␈↓4. ␈↓αProperty Lists␈↓
␈↓ ↓H␈↓␈↓ ¬cCHAPTER IV␈↓ 99
␈↓ ↓H␈↓1. Sequential programs
␈↓ ↓H␈↓2. Side effects
␈↓ ↓H␈↓3. Property lists
␈↓ ↓H␈↓4. Input and output
␈↓ ↓H␈↓5. EXPRS, FEXPRS, LEXPRS, SUBRS, FSUBRS, LEXPRS